a:, b:. b | a  (a rem b) = 0 

latex

Definitions	P  Q, P & Q, P  Q, b | a, x:A. B(x), Prop, A, False, P  Q, a  b, , t  T, , , x:A. B(x), Div(a;n;q), i  j < k, AB, ij, Dec(P), P  Q, {...i}
Lemmas	divide wfa, rem 3 to 1, divides invar 2, minus functionality wrt eq, rem 2 to 1, divides invar 1, rem 4 to 1, decidable le, add mono wrt eq, mul cancel in lt, mul cancel in le, le wf, div elim, nat plus inc int nzero, rem to div, nat wf, nat plus wf, int nzero wf, divides wf